Nuprl Lemma : multiply_functionality_wrt_eqmod
2,24
postcript
pdf
m
,
a
,
a'
,
b
,
b'
:
. (
a
=
a'
mod
m
)
(
b
=
b'
mod
m
)
((
a
b
) = (
a'
b'
) mod
m
)
latex
Definitions
a
=
b
mod
m
,
P
Q
,
b
|
a
,
x
:
A
.
B
(
x
)
,
t
T
,
T
,
True
,
Prop
Lemmas
true
wf
,
squash
wf
,
divisor
of
sum
,
divisor
of
mul
,
divides
wf
origin
m, a, a', b, b':
. (a = a' mod m) 
(b = b' mod m) ((a
b) = (a'b') mod m) m, a, a', b, b':. (a = a' mod m) (b = b' mod m) ((ab) = (a'b') mod m) Qx:A. B(x)
T
T